Nuprl Lemma : unique_set_wf
2,24
postcript
pdf
T
:Type,
P
:(
T
Prop). {!
x
:
T
|
P
(
x
)}
Type
latex
Definitions
{!
x
:
T
|
P
(
x
)}
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
Prop
,
t
T
origin
T:Type, P:(T
Prop). {!x:T | P(x)} 
Type T:Type, P:(TProp). {!x:T | P(x)} Type x:A. B(x)
Q T